\begin{tabbing}
es{-}first{-}at{-}since'(${\it es}$;$i$;$e$;$e$.$R$($e$);$e$.$P$($e$))
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=es{-}loc(${\it es}$; $e$) = $i$ $\in$ Id\+
\\[0ex]\& $R$($e$)
\\[0ex]\& ($\exists$\=${\it e'}$:es{-}E(${\it es}$)\+
\\[0ex](es{-}locl(${\it es}$; ${\it e'}$; $e$)
\\[0ex]c$\wedge$ \=($P$(${\it e'}$)\+
\\[0ex]\& ($\forall$${\it e''}$:es{-}E(${\it es}$). es{-}le(${\it es}$;${\it e'}$;${\it e''}$) $\Rightarrow$ es{-}locl(${\it es}$; ${\it e''}$; $e$) $\Rightarrow$ ($\neg$$R$(${\it e''}$))))))
\-\-\-
\end{tabbing}